(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const r0 Real)
(declare-const r2 Real)
(declare-const r4 Real)
(declare-const r5 Real)
(declare-const r6 Real)
(declare-const r7 Real)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const r10 Real)
(push)
(declare-const v4 Bool)
(pop)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const r11 Real)
(declare-const v7 Bool)
(assert (or (distinct v0 v1 v0 (< r2 r5) (< r2 r5) v0 v0) (not (or v1 (distinct 622987.4956 r4) v0)) v5 v3 (< r6 6221 r4 622987.4956 (/ 6221 r0)) (>= 0.52942554 (/ 6221 r0) r7 r2 r0)))
(assert (or (< r2 r5) (< r2 r5)))
(assert (or v5 (< r2 r5) (or v1 (distinct 622987.4956 r4) v0) (< r2 r5) (or v1 (distinct 622987.4956 r4) v0) (not (or v1 (distinct 622987.4956 r4) v0))))
(assert (or (or v1 (distinct 622987.4956 r4) v0)))
(assert (or (>= (* 2 r5 r7 r7 6221) r0) (distinct v0 v1 v0 (< r2 r5) (< r2 r5) v0 v0)))
(assert (or v5 (xor (>= 0.52942554 (/ 6221 r0) r7 r2 r0) (distinct 622987.4956 r4) v2 (distinct 622987.4956 r4) (< r2 r5) v2 v0) v5 (xor (>= 0.52942554 (/ 6221 r0) r7 r2 r0) (distinct 622987.4956 r4) v2 (distinct 622987.4956 r4) (< r2 r5) v2 v0) v6 (>= 0.52942554 (/ 6221 r0) r7 r2 r0) (< r2 r5)))
(assert (or v5))
(assert (or (< r2 r5) (< r2 r5) v1 v1 v6 (< r6 6221 r4 622987.4956 (/ 6221 r0)) v3 (< r6 6221 r4 622987.4956 (/ 6221 r0))))
(assert (or (xor (>= 0.52942554 (/ 6221 r0) r7 r2 r0) (distinct 622987.4956 r4) v2 (distinct 622987.4956 r4) (< r2 r5) v2 v0)))
(assert (or (not (or v1 (distinct 622987.4956 r4) v0)) (< r6 6221 r4 622987.4956 (/ 6221 r0)) v3 (< r6 6221 r4 622987.4956 (/ 6221 r0))))
(assert (or (not (or v1 (distinct 622987.4956 r4) v0)) v6))
(assert (or (or v1 (distinct 622987.4956 r4) v0) (>= 0.52942554 (/ 6221 r0) r7 r2 r0)))
(assert (or v6 v6))
(assert (or (or v1 (distinct 622987.4956 r4) v0) (>= (* 2 r5 r7 r7 6221) r0)))
(assert (or (distinct v0 v1 v0 (< r2 r5) (< r2 r5) v0 v0) (< r6 6221 r4 622987.4956 (/ 6221 r0)) (< r2 r5) (or v1 (distinct 622987.4956 r4) v0) v5 (distinct v0 v1 v0 (< r2 r5) (< r2 r5) v0 v0) v3 (< r2 r5)))
(assert (or v1 (distinct v0 v1 v0 (< r2 r5) (< r2 r5) v0 v0)))
(assert (or v5 v2))
(assert (or v3))
(check-sat)
